\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Cmd}$:Type, ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)), ${\it Config}$:AbsInterface(chain\_config()),\+
\\[0ex]$u$:(\{$e$:E(${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} $\rightarrow$\{$e$:E$\mid$ ($\uparrow$($e$ $\in_{b}$ ${\it Sys}$)) $\vee$ ($\uparrow$($e$ $\in_{b}$ ${\it Config}$))\} ).
\-\\[0ex]update{-}antecedent\{i:l\}(${\it es}$;${\it Cmd}$;${\it Sys}$;${\it Config}$;$u$)
\\[0ex]$\Rightarrow$ ${\it Sys}$ $\cap$ ${\it Config}$ = 0
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E(${\it Sys}$(valid)).\+
\\[0ex]($\uparrow$csupdate?(${\it Sys}$($e$))) $\Rightarrow$ ($\uparrow$(($u$($e$)) $\in_{b}$ ${\it Config}$)) $\Rightarrow$ ($u$($e$) $\in$ E(prior(${\it Sys}$(valid)))))
\-
\end{tabbing}